FIFO
== C:Type
==  (T:Type
==  S:(CCE)
==  R:(CE)
==  codes:(j,i:Ce:{x:E| S(j,i,x)} state@loc(e)T)
==  (decodes:(i:Ce:{x:E| R(i,x)} state@loc(e)T)
==  for clients C sends FIFO
==  forfrom j to i via (S[j,i],codes)
==  forreceives at i via (R[i],decodes))) 

latex

---

clarification:

FIFO{i:l}
FIFO(es)
== C:Type{i}
==  (T:Type{i}
==  S:(CCes-E(es){i})
==  R:(Ces-E(es){i})
==  codes:(j:Ci:Ce:{x:es-E(es)| S(j,i,x)} es-state(es;es-loc(es; e))T)
==  (decodes:(i:Ce:{x:es-E(es)| R(i,x)} es-state(es;es-loc(es; e))T)
==  fifo(es;codes;decodes;C;S;R;T))) 

latex

Definitions	Type, , x:A  B(x), {x:A| B(x)} , E, f(a), x:AB(x), state@i, loc(e), for clients C sends FIFO   from j to i via (S[j,i],codes)   receives at i via (R[i],decodes)
FDL editor aliases	FIFO